(DEFPROP unify ((case extsubst terms) ts1 ((case extsubst terms) ts2 (pair_unify ts1 ts2) 'NOSUBST) ((case extsubst terms) ts2 'NOSUBST (unify1 (pair_unify (hdterm ts1) (hdterm ts2)) (tlterms ts1) (tlterms ts2)))) BODY)